import scala.io.Source 

class Proof(name: String, bufferDelay: String, inputs: Theorem*) { // Some inputs tied to an and gate. Also there is a buffer.
  var delay = 0 
  def this(name: String) { 
    this(name, "0")  
  }
  def this() { 
    this("unnamed")
  }
  def calcDelay():Int = inputs.foldLeft(0)( (a,b)=> a+b.delay ) + Integer.parseInt(bufferDelay)
  override def toString(): String = "Proof: " + name + " withDelay: " + calcDelay + "\n" + inputs.map(_.toString());
}

class Theorem(name: String, methods: Proof*){ // this is the or gate. 这里的proof*实际上是多个uniq ID of the proof
  var delay = 1 
  def this(name: String) { this(name, new Proof("commonSenseProof") ) } 
  def this(){ this("unnamed") }

  def getAllMethods():String = methods.foldLeft("")( (a:String,b:Proof) => a + b + ";" )

  def calcDelay():Int = methods.foldLeft(0)( (a,b)=> a+b.delay ) -1

  override def toString(): String ={
    "Theorem: \"" + name + "\"\n   has " + methods.length + " proofs withDelay: " + calcDelay + "\n"  + getAllMethods() + "\n\n"
  }
}

class ztry( n: String, m: String) {
  override def toString(): String = n+m
  def zstr( x:String): String = "haha: "+n+m+x
}
object hello extends App {

  val file=Source.fromFile("zrepo_Dont_deleteWholeLine_Dont_addNewLineBeforeSomeLine.scala").mkString.split('\n')

  // 第一行无用，所以号要+1
  val naiveTheorems = file.zipWithIndex.map( x=> x match{ case (a,b)=>(a,b+1)}).map( a=>{ new Theorem( a._2 +"___"  + a._1 ) }) 
  val complexTheorems = file.zipWithIndex.map( x=> x match{ case (a,b)=>(a,b+1)}).filter(b=>b._1.contains("  ")).map( a=>{ // 标志“  ”表示一个复杂定理 
        val proofs:Seq[Proof] = a._1.split("  ").drop(1).map( aNameCountAndTheorem => { // 此定理用到的所有proofs。第一项是定理的名字，要删除。
          val name= aNameCountAndTheorem.split(' ')(0) // 每个证明的格式：名 用到定理数 用到的定理的号*
          val count = aNameCountAndTheorem.split(' ')(1)
          val theoremsUsedByThisProof:Seq[Theorem] = aNameCountAndTheorem.split(' ').drop(2).map( ab=> naiveTheorems(Integer.parseInt(ab)-1).asInstanceOf[Theorem] )
          Class.forName( "Proof").getConstructors()(2).newInstance( name, count, theoremsUsedByThisProof ).asInstanceOf[Proof] // 返回当前定理用的一个证明
        }) // map之后，由一个变多个证明
        //println("此定理的所有证明方法:")
        //proofs foreach println
        new Theorem( a._2 +"___"  + a._1.split("  ")(0),  proofs:_*)  // Seq to individuals手法。 生成一个定理对象。0表示定理的名字。
        //new Theorem("Great",  new Proof("proof1", "2",  naiveTheorems(6), naiveTheorems(4) ), new Proof("proof2", "2",  naiveTheorems(6), naiveTheorems(4) ) )
  }) 
  complexTheorems foreach  println
  /*
  // 
      val c2 = Class.forName("Proof")
          val constructor = c2.getConstructor(classOf[String], classOf[String])
              val obj2 = constructor.newInstance("person", "China").asInstanceOf[Person]
  */

/* zrepo_Dont_deleteWholeLine_Dont_addNewLineBeforeSomeLine
  val naiveTheorems = List(
    new Theorem("Seq has countably many elements"),
    new Theorem("We can choose subsequence"),
    new Theorem("There is a real/rational between two reals"),

    new Theorem("0 iff < epsilon"),
    new Theorem("有界指的是sup和inf全是实数"),
    new Theorem("Bounded infinity points has limit point"),

    new Theorem("数集元素越多，则sup越大"),
    new Theorem("nothing")
  )
  */

//  naiveTheorems foreach println 

/*
  val t1 = new Theorem("有界数列的子列，仍有界", new Proof("proof1", 2,  naiveTheorems(6), naiveTheorems(4) ))
  //val t1 = new Theorem("Subsequence of a bounded seq. is also ...", new Proof("proof1", 2,  naiveTheorems(6), naiveTheorems(4) ))
  println(t1)
  */

}
